MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { g() -> h() , h() -> g() , c() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. Trs: { c() -> d() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(g) = {}, safe(h) = {}, safe(c) = {}, safe(d) = {} and precedence g ~ h, g ~ c, h ~ c . Following symbols are considered recursive: {} The recursion depth is 0. For your convenience, here are the satisfied ordering constraints: g() >= h() h() >= g() c() > d() We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { g() -> h() , h() -> g() } Weak Trs: { c() -> d() } Obligation: innermost runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..